/*!
 * \file symbol_table_test.cc
 *
 * \brief Symbol Table testing
 *
 * This file tests the symbol table and the expression vector classes and their
 * methods
 *
 * \date Started: 7/8/2010
 * \date Last Modified: 7/27/2010
 * \authors Alan LaMielle
 * \authors Ian Craig
 */

#include <iegenlib/iegenlib.h>

#include <gtest/gtest.h>
#include <set>
using std::set;
#include <utility>
using std::pair;
using std::make_pair;

using iegenlib::StringException;

using iegenlib::TUPLE;
using iegenlib::EXISTENTIAL;
using iegenlib::SYMBOLIC;
using iegenlib::UFCALL;
using iegenlib::CONST;

using iegenlib::SymbolTable;
using iegenlib::ExpVec;
using iegenlib::UFCall;
using iegenlib::STE;
using iegenlib::TupleType;

//Tests that the ExpVec assignment operator doesn't reduce the size of vectors
TEST(ExpVec,AssignmentOperator){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("a");

  SymbolTable st(&varTuple, &symbolics, &exists, 0);
  ExpVec a_exp_before=st.constructExpVec("a",1);

  EXPECT_EQ(1,a_exp_before.get_tuplevars_size());
  EXPECT_EQ(0,a_exp_before.get_ufcalls_size());

  EXPECT_EQ(0,st.getNumFuncs());
  UFCall* ufcall=st.lookup("f",list<ExpVec>(1,a_exp_before));
  EXPECT_EQ(1,st.getNumFuncs());

  ExpVec a_exp_after(st.constructExpVec());

  EXPECT_EQ(1,a_exp_after.get_tuplevars_size());
  EXPECT_EQ(1,a_exp_after.get_ufcalls_size());

  a_exp_after=a_exp_after.copy_coeff(a_exp_before);

  EXPECT_EQ(1,a_exp_after.get_tuplevars_size());
  EXPECT_EQ(1,a_exp_after.get_ufcalls_size());
}

//Tests that the ExpVec addition operator doesn't reduce the size of vectors
TEST(ExpVec,AdditionOperator1){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("a");

  SymbolTable st(&varTuple, &symbolics, &exists, 0);
  ExpVec a_exp_before=st.constructExpVec("a",1);

  EXPECT_EQ(1,a_exp_before.get_tuplevars_size());
  EXPECT_EQ(0,a_exp_before.get_ufcalls_size());
  EXPECT_EQ(1,a_exp_before.get_coeff(TUPLE,0));

  EXPECT_EQ(0,st.getNumFuncs());
  UFCall* ufcall=st.lookup("f",list<ExpVec>(1,a_exp_before));
  EXPECT_EQ(1,st.getNumFuncs());

  ExpVec a_exp_after(st.constructExpVec());

  EXPECT_EQ(1,a_exp_after.get_tuplevars_size());
  EXPECT_EQ(1,a_exp_after.get_ufcalls_size());
  EXPECT_EQ(0,a_exp_after.get_coeff(TUPLE,0));
  EXPECT_EQ(0,a_exp_after.get_coeff(UFCALL,0));

  a_exp_after.set_coeff(UFCALL,0,2);

  ExpVec sum=a_exp_before+a_exp_after;

  EXPECT_EQ(1,sum.get_tuplevars_size());
  EXPECT_EQ(1,sum.get_ufcalls_size());
  EXPECT_EQ(1,sum.get_coeff(TUPLE,0));
  EXPECT_EQ(2,sum.get_coeff(UFCALL,0));
}

//Tests that the ExpVec addition operator doesn't reduce the size of vectors
TEST(ExpVec,AdditionOperator2){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("a");

  SymbolTable st(&varTuple, &symbolics, &exists, 0);
  ExpVec a_exp_before=st.constructExpVec("a",1);

  EXPECT_EQ(1,a_exp_before.get_tuplevars_size());
  EXPECT_EQ(0,a_exp_before.get_ufcalls_size());
  EXPECT_EQ(1,a_exp_before.get_coeff(TUPLE,0));

  EXPECT_EQ(0,st.getNumFuncs());
  UFCall* ufcall=st.lookup("f",list<ExpVec>(1,a_exp_before));
  EXPECT_EQ(1,st.getNumFuncs());

  ExpVec a_exp_after(st.constructExpVec());

  EXPECT_EQ(1,a_exp_after.get_tuplevars_size());
  EXPECT_EQ(1,a_exp_after.get_ufcalls_size());
  EXPECT_EQ(0,a_exp_after.get_coeff(TUPLE,0));
  EXPECT_EQ(0,a_exp_after.get_coeff(UFCALL,0));

  a_exp_after.set_coeff(UFCALL,0,2);

  ExpVec sum=a_exp_after+a_exp_before;

  EXPECT_EQ(1,sum.get_tuplevars_size());
  EXPECT_EQ(1,sum.get_ufcalls_size());
  EXPECT_EQ(1,sum.get_coeff(TUPLE,0));
  EXPECT_EQ(2,sum.get_coeff(UFCALL,0));
}

//Tests that the ExpVec.set_coeff method raises an exception when given the
// CONST constant for type
TEST(ExpVec, SetCoeffNoCONST){
  bool fail=true;
  try{
    set<string> varTuple,symbolics,exists;
    SymbolTable st(&varTuple, &symbolics, &exists, 0);
    ExpVec v=st.constructExpVec();
    v.set_coeff(CONST,0,15);
  }
  catch(StringException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"ExpVec.set_coeff does not raise an exception when setting the coefficient for CONST";
  }
}

//Tests that the ExpVec.get_coeff method raises an exception when given the
// CONST constant for type
TEST(ExpVec, GetCoeffNoCONST){
  bool fail=true;
  try{
    set<string> varTuple,symbolics,exists;
    SymbolTable st(&varTuple, &symbolics, &exists, 0);
    ExpVec v=st.constructExpVec();
    v.get_coeff(CONST,0);
  }
  catch(StringException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"ExpVec.get_coeff does not raise an exception when setting the coefficient for CONST";
  }
}

//Tests the ExpVec.normalizeEquality() method
TEST(ExpVec,NormalizeEquality1){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  SymbolTable st(&varTuple, &symbolics, &exists, 0);

  ExpVec EV1 = st.constructExpVec("var1",1);
  ExpVec EV2 = st.constructExpVec("var1",-1);
  EV2.normalizeEquality();

  EXPECT_TRUE(EV1 == EV2);
}

//Test for bug #410
TEST(ExpVec,NormalizeEquality2){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("var1");
  SymbolTable st(&varTuple, &symbolics, &exists, 0);

  ExpVec EV1 = st.constructExpVec("var1",1);
  EV1.set_const(10);
  ExpVec EV2 = st.constructExpVec("var1",-1);
  EV2.set_const(-10);
  EV2.normalizeEquality();

  EXPECT_TRUE(EV1 == EV2);
}

//Tests the ExpVec.any() method with tuple variables
TEST(ExpVec, Any){
  set<string> varTuple;
  varTuple.insert("var1");
  set<string> symbolics;
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 2);

  ExpVec v=st.constructExpVec();
  int pos,coeff;
  bool res;

  //No coefficients have been set
  EXPECT_EQ(v.any(SYMBOLIC,pos,coeff),false);
  EXPECT_EQ(v.any(TUPLE,pos,coeff),false);
  EXPECT_EQ(v.any(EXISTENTIAL,pos,coeff),false);
  EXPECT_EQ(v.any(UFCALL,pos,coeff),false);
  EXPECT_EQ(v.any(CONST,pos,coeff),false);

  //Just var1=1 has been set
  v=st.constructExpVec("var1",1);
  EXPECT_EQ(v.any(SYMBOLIC,pos,coeff),false);
  EXPECT_EQ(v.any(EXISTENTIAL,pos,coeff),false);
  EXPECT_EQ(v.any(UFCALL,pos,coeff),false);
  EXPECT_EQ(v.any(CONST,pos,coeff),false);
  res=v.any(TUPLE,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,1);

  //exist1=-6, ufcall 1 = 3, and const=22
  v.set_coeff(EXISTENTIAL,0,-6);
  v.set_coeff(UFCALL,1,3);
  v.set_const(22);
  EXPECT_EQ(v.any(SYMBOLIC,pos,coeff),false);
  res=v.any(TUPLE,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,1);
  res=v.any(EXISTENTIAL,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,-6);
  res=v.any(UFCALL,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,1);
  EXPECT_EQ(coeff,3);
  res=v.any(CONST,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(coeff,22);

  ExpVec exist1_exp=st.constructExpVec("exist1",1);
  STE* g_of_exist1=st.lookup("g",list<ExpVec>(1,exist1_exp));

  v=st.constructExpVec("g",list<ExpVec>(1,exist1_exp),1);
  res=v.any(UFCALL,0);
  EXPECT_TRUE(res);
  res=v.any(EXISTENTIAL,0);
  EXPECT_FALSE(res);
  res=v.any(EXISTENTIAL,0,&st);
  EXPECT_TRUE(res);

  list<ExpVec> f_params;
  f_params.push_back(st.constructExpVec(2));
  f_params.push_back(v);
  STE* f_of_2_g_of_exist1=st.lookup("f",f_params);
  v=st.constructExpVec("f",f_params,1);
  res=v.any(UFCALL,1);
  EXPECT_TRUE(res);
  res=v.any(EXISTENTIAL,0);
  EXPECT_FALSE(res);
  res=v.any(EXISTENTIAL,0,&st);
  EXPECT_TRUE(res);
}

TEST(ExpVec,ReplaceExistential){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("a");
  exists.insert("e");
  symbolics.insert("n");
  SymbolTable st(&varTuple, &symbolics, &exists, 0);

  ExpVec e=st.constructExpVec();
  e.set_coeff(SYMBOLIC,0,2);
  e.set_coeff(TUPLE,0,4);
  e.set_coeff(EXISTENTIAL,0,-3);
  e.set_const(2);

  ExpVec rep=st.constructExpVec();
  rep.set_coeff(SYMBOLIC,0,-3);
  rep.set_coeff(TUPLE,0,4);
  rep.set_const(2);

  ExpVec res=st.constructExpVec();
  res.set_coeff(SYMBOLIC,0,11);
  res.set_coeff(TUPLE,0,-8);
  res.set_const(-4);

  EXPECT_EQ(e.replaceExistential(&st,0,rep),res);
}

TEST(ExpVec,IsAffine){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("a");
  exists.insert("e");
  symbolics.insert("n");
  SymbolTable st(&varTuple, &symbolics, &exists, 1);
  ExpVec a(st.constructExpVec("a",1));
  st.lookup("f",list<ExpVec>(1,a));

  EXPECT_TRUE(st.constructExpVec("a",1).isAffine());
  EXPECT_TRUE(st.constructExpVec("a",-1).isAffine());
  EXPECT_TRUE(st.constructExpVec("a",3).isAffine());
  EXPECT_TRUE(st.constructExpVec("a",-3).isAffine());

  EXPECT_TRUE(st.constructExpVec("e",1).isAffine());
  EXPECT_TRUE(st.constructExpVec("e",-1).isAffine());
  EXPECT_TRUE(st.constructExpVec("e",3).isAffine());
  EXPECT_TRUE(st.constructExpVec("e",-3).isAffine());

  EXPECT_TRUE(st.constructExpVec("n",1).isAffine());
  EXPECT_TRUE(st.constructExpVec("n",-1).isAffine());
  EXPECT_TRUE(st.constructExpVec("n",3).isAffine());
  EXPECT_TRUE(st.constructExpVec("n",-3).isAffine());

  ExpVec f_of_a(st.constructExpVec());

  f_of_a.set_coeff(UFCALL,0,1);
  EXPECT_FALSE(f_of_a.isAffine());
  f_of_a.set_coeff(UFCALL,0,-1);
  EXPECT_FALSE(f_of_a.isAffine());

  f_of_a.set_coeff(UFCALL,0,3);
  EXPECT_FALSE(f_of_a.isAffine());
  f_of_a.set_coeff(UFCALL,0,-3);
  EXPECT_FALSE(f_of_a.isAffine());
}

TEST(ExpVec,IsAffineNoUFSCols){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("a");
  SymbolTable st(&varTuple, &symbolics, &exists, 0);

  EXPECT_TRUE(st.constructExpVec("a",1).isAffine());
}

TEST(ExpVec,IsAffineTwoUFSCols){
  set<string> varTuple,symbolics,exists;
  varTuple.insert("a");
  varTuple.insert("b");
  SymbolTable st(&varTuple, &symbolics, &exists, 2);
  ExpVec a(st.constructExpVec("a",1));
  st.lookup("f",list<ExpVec>(1,a));
  ExpVec b(st.constructExpVec("b",1));
  st.lookup("f",list<ExpVec>(1,b));

  EXPECT_TRUE(st.constructExpVec("a",1).isAffine());
  EXPECT_TRUE(st.constructExpVec("a",-1).isAffine());
  EXPECT_TRUE(st.constructExpVec("b",1).isAffine());
  EXPECT_TRUE(st.constructExpVec("b",-1).isAffine());

  ExpVec f_of_a(st.constructExpVec());
  ExpVec f_of_b(st.constructExpVec());

  f_of_a.set_coeff(UFCALL,0,1);
  EXPECT_FALSE(f_of_a.isAffine());
  f_of_a.set_coeff(UFCALL,0,-1);
  EXPECT_FALSE(f_of_a.isAffine());

  f_of_b.set_coeff(UFCALL,1,1);
  EXPECT_FALSE(f_of_b.isAffine());
  f_of_b.set_coeff(UFCALL,1,-1);
  EXPECT_FALSE(f_of_b.isAffine());

  f_of_a.set_coeff(UFCALL,1,1);
  EXPECT_FALSE(f_of_a.isAffine());
  f_of_a.set_coeff(UFCALL,1,-1);
  EXPECT_FALSE(f_of_a.isAffine());
}

//This particular test is based off of the column values of some
//vartuple tokens. Each one should have their own specific number, so when
//placed into a set, there should be three of them. We cannot test the number
//itself because the symbol table won't know them in particular (and nor will
//other classes), but if we still should end up with three unique numbers.
TEST(SymbolTable, TupleColumnTest){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  list<pair<string, int> > conVal;
  set<string> temp;
  SymbolTable st(&varTuple, &temp, &temp, 0);

  STE* v1 = st.lookup("var1");
  STE* v2 = st.lookup("var2");
  STE* v3 = st.lookup("var3");

  set<int> varColSet;
  varColSet.insert(v1->getCol());
  varColSet.insert(v2->getCol());
  varColSet.insert(v3->getCol());

  EXPECT_EQ(varColSet.size(), 3);
}

//This test follows the same pattern as the one above but tests symbolics
//instead of vartuples
TEST(SymbolTable, SymbolicColumnTest){
  set<string> symbolics;
  symbolics.insert("var1");
  symbolics.insert("var2");
  symbolics.insert("var3");
  list<pair<string, int> > conVal;
  set<string> temp1;
  SymbolTable st(&temp1, &symbolics, &temp1, 0);

  STE* v1 = st.lookup("var1");
  STE* v2 = st.lookup("var2");
  STE* v3 = st.lookup("var3");

  set<int> varColSet;
  varColSet.insert(v1->getCol());
  varColSet.insert(v2->getCol());
  varColSet.insert(v3->getCol());

  EXPECT_EQ(varColSet.size(), 3);
}

//This test follows the same patter as the ones above but tests existential
//variables instead of symbolics or vartuples
TEST(SymbolTable, ExistentialColumnTest){
  set<string> exists;
  exists.insert("var1");
  exists.insert("var2");
  exists.insert("var3");
  list<pair<string, int> > conVal;
  set<string> temp1;
  SymbolTable st(&temp1, &temp1, &exists, 0);

  STE* v1 = st.lookup("var1");
  STE* v2 = st.lookup("var2");
  STE* v3 = st.lookup("var3");

  set<int> varColSet;
  varColSet.insert(v1->getCol());
  varColSet.insert(v2->getCol());
  varColSet.insert(v3->getCol());

  EXPECT_EQ(varColSet.size(), 3);
}

//This test follows the a similar pattern as the ones above but with a
//combination of vartuples, symbolics, or existential variables.
TEST(SymbolTable, MultipleColumnTest){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  set<string> temp1;
  SymbolTable st1(&varTuple, &symbolics, &temp1, 0);

  STE* v1 = st1.lookup("var1");
  STE* v2 = st1.lookup("var2");
  STE* v3 = st1.lookup("var3");

  STE* s1 = st1.lookup("sym1");
  STE* s2 = st1.lookup("sym2");
  STE* s3 = st1.lookup("sym3");

  set<int> varColSet;
  varColSet.insert(v1->getCol());
  varColSet.insert(v2->getCol());
  varColSet.insert(v3->getCol());

  set<int> symColSet;
  symColSet.insert(s1->getCol());
  symColSet.insert(s2->getCol());
  symColSet.insert(s3->getCol());

  EXPECT_EQ(varColSet.size(), 3);
  EXPECT_EQ(symColSet.size(), 3);
  varColSet.clear();
  symColSet.clear();

  SymbolTable st2(&temp1, &symbolics, &exists, 0);

  s1 = st2.lookup("sym1");
  s2 = st2.lookup("sym2");
  s3 = st2.lookup("sym3");

  STE* e1 = st2.lookup("exist1");
  STE* e2 = st2.lookup("exist2");
  STE* e3 = st2.lookup("exist3");

  symColSet.insert(s1->getCol());
  symColSet.insert(s2->getCol());
  symColSet.insert(s3->getCol());

  set<int> existsColSet;
  existsColSet.insert(e1->getCol());
  existsColSet.insert(e2->getCol());
  existsColSet.insert(e3->getCol());

  EXPECT_EQ(symColSet.size(), 3);
  EXPECT_EQ(existsColSet.size(), 3);
  symColSet.clear();
  existsColSet.clear();

  SymbolTable st3(&varTuple, &temp1, &exists, 0);

  v1 = st3.lookup("var1");
  v2 = st3.lookup("var2");
  v3 = st3.lookup("var3");

  e1 = st2.lookup("exist1");
  e2 = st2.lookup("exist2");
  e3 = st2.lookup("exist3");

  varColSet.insert(v1->getCol());
  varColSet.insert(v2->getCol());
  varColSet.insert(v3->getCol());

  existsColSet.insert(e1->getCol());
  existsColSet.insert(e2->getCol());
  existsColSet.insert(e3->getCol());

  EXPECT_EQ(varColSet.size(), 3);
  EXPECT_EQ(existsColSet.size(), 3);
}

//This test follows the same pattern as the one above but with a combination
//of all three variable types.
TEST(SymbolTable, FullColumnTest){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 0);

  STE* v1 = st.lookup("var1");
  STE* v2 = st.lookup("var2");
  STE* v3 = st.lookup("var3");

  STE* s1 = st.lookup("sym1");
  STE* s2 = st.lookup("sym2");
  STE* s3 = st.lookup("sym3");

  STE* e1 = st.lookup("exist1");
  STE* e2 = st.lookup("exist2");
  STE* e3 = st.lookup("exist3");

  set<int> varColSet;
  varColSet.insert(v1->getCol());
  varColSet.insert(v2->getCol());
  varColSet.insert(v3->getCol());

  set<int> symColSet;
  symColSet.insert(s1->getCol());
  symColSet.insert(s2->getCol());
  symColSet.insert(s3->getCol());

  set<int> existColSet;
  existColSet.insert(e1->getCol());
  existColSet.insert(e2->getCol());
  existColSet.insert(e3->getCol());

  EXPECT_EQ(varColSet.size(), 3);
  EXPECT_EQ(symColSet.size(), 3);
  EXPECT_EQ(existColSet.size(), 3);
}

//This test deals with the expression vector and its methods (most importantly
//the toString(symtable) method. We can test the entire string in this rare case
//because we set the coefficients ourselves.
TEST(SymbolTable, ExpConstructs){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

  st.lookup("func1",list<ExpVec>());

  ExpVec EV1 = st.constructExpVec();
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(SYMBOLIC, i, 1); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(TUPLE, i, 2); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(EXISTENTIAL, i, -2); }
  EV1.set_coeff(UFCALL, 0, -1);

  EXPECT_EQ("sym1+sym2+sym3+2var1+2var2+2var3-2exist1-2exist2-2exist3-func1", EV1.toString(&st));
}

//This test follows the ones as above, but instead tests to make sure that if
//there is more than one variable, symbolic, or existential of the same name
//that the column information still retains the correct location.
TEST(SymbolTable, DuplicateColTest){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 0);

  STE* v1 = st.lookup("var1");
  STE* v2 = st.lookup("var1");
  STE* v3 = st.lookup("var1");

  STE* s1 = st.lookup("sym1");
  STE* s2 = st.lookup("sym1");
  STE* s3 = st.lookup("sym1");

  STE* e1 = st.lookup("exist1");
  STE* e2 = st.lookup("exist1");
  STE* e3 = st.lookup("exist1");

  set<int> varColSet;
  varColSet.insert(v1->getCol());
  varColSet.insert(v2->getCol());
  varColSet.insert(v3->getCol());

  set<int> symColSet;
  symColSet.insert(s1->getCol());
  symColSet.insert(s2->getCol());
  symColSet.insert(s3->getCol());

  set<int> existColSet;
  existColSet.insert(e1->getCol());
  existColSet.insert(e2->getCol());
  existColSet.insert(e3->getCol());

  EXPECT_EQ(varColSet.size(), 1);
  EXPECT_EQ(symColSet.size(), 1);
  EXPECT_EQ(existColSet.size(), 1);
}

class SymbolTableMerging:public::testing::Test{
public:
  SymbolTable* st;
  list<TupleType> tuples;
  list<string> all;
  list<ExpVec> funcF;
  list<ExpVec> funcG;
  list<ExpVec> funcH;
protected:
  virtual void SetUp(){
    set<string> varTuple;
    varTuple.insert("var1");
    all.push_back("var1");
    varTuple.insert("var2");
    all.push_back("var2");
    varTuple.insert("var3");
    all.push_back("var3");
    set<string> symbolics;
    symbolics.insert("sym1");
    all.push_back("sym1");
    symbolics.insert("sym2");
    all.push_back("sym2");
    symbolics.insert("sym3");
    all.push_back("sym3");
    set<string> exists;
    exists.insert("exist1");
    all.push_back("exist1");
    exists.insert("exist2");
    all.push_back("exist2");
    exists.insert("exist3");
    all.push_back("exist3");
    list<pair<string, int> > conVal;
    st = new SymbolTable(&varTuple, &symbolics, &exists, 3);
    funcF.push_back(st->constructExpVec("var1", 1));
    st->lookup("f",funcF);
    all.push_back("f");
    funcG.push_back(st->constructExpVec("var2", 1));
    st->lookup("g",funcG);
    all.push_back("g");
    funcH.push_back(st->constructExpVec("var3", 1));
    st->lookup("h",funcH);
    all.push_back("h");

    tuples.push_back(TupleType("var1"));
    tuples.push_back(TupleType("var2"));
    tuples.push_back(TupleType("var3"));
  }

  virtual void TearDown(){
    delete st;
  }
};

TEST_F(SymbolTableMerging, convertExpVecTests){
  ExpVec fullEV = st->constructExpVec("var1", 1) +
  st->constructExpVec("var2", 2) +
  st->constructExpVec("var3", 3) +
  st->constructExpVec("sym1", 4) +
  st->constructExpVec("sym2", 5) +
  st->constructExpVec("sym3", 6) +
  st->constructExpVec("exist1", 7) +
  st->constructExpVec("exist2", 8) +
  st->constructExpVec("exist3", 9);

  set<string> tuples2;
  set<string> exists2;
  set<string> symbolics2;
  map<string,string> symbolMap;

  tuples2.insert("a");
  tuples2.insert("b");
  tuples2.insert("c");
  exists2.insert("exist1");
  exists2.insert("exist2");
  exists2.insert("exist3");
  symbolics2.insert("sym1");
  symbolics2.insert("sym2");
  symbolics2.insert("sym3");
  symbolMap["var3"] = "a";
  symbolMap["var2"] = "b";
  symbolMap["var1"] = "c";


  SymbolTable* st2 = new SymbolTable(&tuples2, &symbolics2, &exists2, 3);

  ExpVec testVec = st->convertExpVec(fullEV, st2, &symbolMap);

  EXPECT_EQ("4sym1+5sym2+6sym3+3a+2b+c+7exist1+8exist2+9exist3", testVec.toString(st2));
  list<ExpVec> funcF2;
  funcF2.push_back(st2->constructExpVec("c", 1));
  st2->lookup("f",funcF2);
  list<ExpVec> funcG2;
  funcG2.push_back(st2->constructExpVec("b", 1));
  st2->lookup("g",funcG2);
  list<ExpVec> funcH2;
  funcH2.push_back(st2->constructExpVec("a", 1));
  st2->lookup("h",funcH2);

  fullEV = fullEV + st->constructExpVec("f", funcF, 1) +
  st->constructExpVec("g", funcG, 1) +
  st->constructExpVec("h", funcH, 1);
  ExpVec testVec2 = st->convertExpVec(fullEV, st2, &symbolMap);

  EXPECT_EQ("4sym1+5sym2+6sym3+3a+2b+c+7exist1+8exist2+9exist3+f(c)+g(b)+h(a)", testVec2.toString(st2));

  delete st2;
}

//This test deals with the iterator for the symbolics
TEST(SymbolTable, itsyms){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

  st.lookup("func1",list<ExpVec>());

  ExpVec EV1 = st.constructExpVec();
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(SYMBOLIC, i, 1); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(TUPLE, i, 2); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(EXISTENTIAL, i, -2); }
  EV1.set_coeff(UFCALL, 0, -1);

  string itersym;
  for(list<STE*>::const_iterator it = st.symBegin(); it != st.symEnd(); it++){
      itersym += (*it)->getId();
  }

  EXPECT_EQ("sym1sym2sym3", itersym);
}

//This test deals with the iterator for the symbolics
TEST(SymbolTable, itext){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

  st.lookup("func1",list<ExpVec>());

  ExpVec EV1 = st.constructExpVec();
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(SYMBOLIC, i, 1); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(TUPLE, i, 2); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(EXISTENTIAL, i, -2); }
  EV1.set_coeff(UFCALL, 0, -1);

  string iterext;
  for(list<STE*>::const_iterator it = st.existBegin(); it != st.existEnd(); it++){
      iterext += (*it)->getId();
  }

  EXPECT_EQ("exist1exist2exist3", iterext);
}

//This test deals with the iterator for the symbolics
TEST(SymbolTable, itsymsthenext){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

  st.lookup("func1",list<ExpVec>());

  ExpVec EV1 = st.constructExpVec();
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(SYMBOLIC, i, 1); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(TUPLE, i, 2); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(EXISTENTIAL, i, -2); }
  EV1.set_coeff(UFCALL, 0, -1);

  st.existBegin();
  string itersym;
  for(list<STE*>::const_iterator it = st.symBegin(); it != st.symEnd(); it++){
      itersym += (*it)->getId();
  }

  EXPECT_EQ("sym1sym2sym3", itersym);
}

TEST(MemoryLeakTest, functionLeak){
  set<string> varTuple;
  varTuple.insert("x");
  varTuple.insert("y");
  varTuple.insert("z");
  set<string> temp;
  SymbolTable st(&varTuple, &temp, &temp, 1);
  list<ExpVec> params;
  params.push_back(st.constructExpVec("x", 1));
  params.push_back(st.constructExpVec("x", 1));
  params.push_back(st.constructExpVec("x", 1));
  ExpVec function = st.constructExpVec("f", params, 1);

  EXPECT_EQ("f(x,x,x)", function.toString(&st));
}

//This test deals with the iterator for the symbolics
TEST(SymbolTable, numSTE2){
  set<string> varTuple;
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

  st.lookup("func1",list<ExpVec>());

  ExpVec EV1 = st.constructExpVec();
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(SYMBOLIC, i, 1); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(EXISTENTIAL, i, -2); }
  EV1.set_coeff(UFCALL, 0, -1); 

  EXPECT_EQ(7, st.numSTE());
}


//This test deals with the iterator for the ids
TEST(SymbolTable, numSTE4){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

  st.lookup("func1",list<ExpVec>());

  ExpVec EV1 = st.constructExpVec();
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(SYMBOLIC, i, 1); }
  for(int i = 0; i < 3; ++i) { EV1.set_coeff(EXISTENTIAL, i, -2); }
  EV1.set_coeff(UFCALL, 0, -1); 

  list<string> temp;
  temp.push_back("var1"); temp.push_back("var2"); temp.push_back("var3");
  temp.push_back("sym1"); temp.push_back("sym2"); temp.push_back("sym3");
  temp.push_back("exist1"); temp.push_back("exist2"); temp.push_back("exist3");
  list<string> fromst (st.getIdBegin(),st.getIdEnd());
  EXPECT_EQ(fromst.size(), 10);
}

//This test deals with the iterator for the symbolics
TEST(SymbolTable, numSTE3){
  set<string> varTuple;
  set<string> symbolics;
  set<string> exists;
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 0);

  EXPECT_EQ(0, st.numSTE());
}

TEST(SymbolTable, copy1){
  set<string> varTuple;
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

 
  st.lookup("func1",list<ExpVec>());
  SymbolTable scp(st);
 
  EXPECT_EQ(scp.toString(), st.toString());
}

TEST(SymbolTable, copy2){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  symbolics.insert("sym4");
  symbolics.insert("sym5");
  symbolics.insert("sym6");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

 
  st.lookup("func1",list<ExpVec>());
  SymbolTable scp(st);

  SymbolTable spc2 = scp;

  EXPECT_EQ(scp.toString(), spc2.toString());
}

TEST(SymbolTable, copy3){
  set<string> varTuple;
  varTuple.insert("var1");
  varTuple.insert("var2");
  varTuple.insert("var3");
  set<string> symbolics;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym3");
  symbolics.insert("sym4");
  symbolics.insert("sym5");
  symbolics.insert("sym6");
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 1);

 
  st.lookup("func1",list<ExpVec>());

  set<string> varTuple2;
  varTuple.insert("var1");
  set<string> symbolics2;
  symbolics.insert("sym1");
  symbolics.insert("sym2");
  symbolics.insert("sym2.1");
  symbolics.insert("sym3");
  symbolics.insert("sym4");
  symbolics.insert("sym5");
  symbolics.insert("sym6");
  symbolics.insert("sym7");
  symbolics.insert("sym8");
  symbolics.insert("sym9");
  set<string> exists2;
  exists.insert("exist1");
  exists.insert("exist2");
  exists.insert("exist3");
  exists.insert("exist4");
  exists.insert("exist5");
  SymbolTable scp2(&varTuple2, &symbolics2, &exists2, 3);
  scp2.lookup("func1",list<ExpVec>());
  scp2.lookup("func2",list<ExpVec>());
  scp2.lookup("func3",list<ExpVec>());

   {//used so the scp will go out of scope and it can delete
   SymbolTable scp(st);
   SymbolTable s4 = st;
   EXPECT_EQ(s4.toString(), st.toString());
   s4 = scp2;
   EXPECT_EQ(scp2.toString(), s4.toString());
   scp2 = scp;
   EXPECT_EQ(scp2.toString(), scp.toString());
   }
  EXPECT_EQ(scp2.toString(), st.toString());
}
